Section: Software

The AstréeA Static Analyzer of Asynchronous Software

Participants : Patrick Cousot [project scientifique leader, correspondent] , Radhia Cousot, Jérôme Feret, Antoine Miné, Xavier Rival.

AstréeA is a static analyzer prototype for parallel software based on abstract interpretation [39] , [40] , [32] . It started with support from Thésée ANR project (2006–2010) and is continuing within the AstréeA project (2012–2015).

The AstréeA prototype http://www.astreea.ens.fr/ is a fork of the Astrée static analyzer (see 5.2 ) that adds support for analyzing parallel embedded C software.

AstréeA analyzes C programs composed of a fixed set of threads that communicate through a shared memory and synchronization primitives (mutexes, FIFOs, blackboards, etc.), but without recursion nor dynamic creation of memory, threads nor synchronization objects. AstréeA assumes a real-time scheduler, where thread scheduling strictly obeys the fixed priority of threads. Our model follows the ARINC 653 OS specification used in embedded industrial aeronautic software. Additionally, AstréeA employs a weakly-consistent memory semantics to model memory accesses not protected by a mutex, in order to take into account soundly hardware and compiler-level program transformations (such as optimizations). AstréeA checks for the same run-time errors as Astrée , with the addition of data-races.

Compared to Astrée , AstréeA features: a new iterator to compute thread interactions, a refined memory abstraction that takes into account the effect of interfering threads, and a new scheduler partitioning domain. This last domain allows discovering and exploiting mutual exclusion properties (enforced either explicitly through synchronization primitives, or implicitly by thread priorities) to achieve a precise analysis.

AstréeA is currently being applied to analyze a large industrial avionic software: 1.6 MLines of C and 15 threads, completed with a 2,500-line model of the ARINC 653 OS developed for the analysis. The analysis currently takes 29h on a 2.66 GHz 64-bit intel server using one core and generates around 1,800 alarms. The low computation time (only a few times larger than the analysis time by Astrée of synchronous programs of a similar size and structure) shows the scalability of the approach (in particular, we avoid the usual combinatorial explosion associated to thread interleavings). Precision-wise, the result, while not as impressive as that of Astrée , is quite encouraging. Improvements were made this year concerning the precision of AstréeA (from 7,600 alarms in 2010 to 1,800 now) and will continue within the scope of the AstréeA ANR project (Section  8.1.1.2 ).

The details of the analysis are described in [22] .